A:Type, B, C, D:(AType), f:a:A fp B(a), g:a:A fp C(a), eq:EqDecider(A).
(a:A. a  dom(f)  B(a)  D(a))
 (a:A. a  dom(g)  C(a)  D(a))
 f  g  a:A fp D(a) 

latex

Definitions	f  g, Top, EqDecider(T), x. t(x), a:A fp B(a), S  T, (x  l), x(s), S  T, x  dom(f), SqStable(P), T, True, b, deq-member(eq;x;L), t  T, P  Q, P & Q, x:A. B(x), P  Q, P  Q
Lemmas	assert-deq-member, deq-member wf, assert wf, decidable assert, sq stable from decidable, l member wf, fpf wf, deq wf, fpf-trivial-subtype-top, fpf-dom wf, fpf-join wf